Lemma equation_subst:
  forall a b: Set, a = b -> b = a.
Proof.
  intros.
  subst.
  reflexivity.
Qed.